\begin{tabbing}
$\forall$$P_{1}$:(es\_realizer\{i:l\}$\rightarrow$prop\{i':l\}). 
\\[0ex]$P_{1}$(Rnone)
\\[0ex]$\Rightarrow$ ($\forall$${\it left}$,${\it right}$:es\_realizer\{i:l\}. $P_{1}$(${\it left}$) $\Rightarrow$ $P_{1}$(${\it right}$) $\Rightarrow$ $P_{1}$(Rplus(${\it left}$; ${\it right}$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $T$:Type\{i\}, $x$:Id, $v$:($T$ + (rationals$\rightarrow$$T$)). $P_{1}$(Rinit(${\it loc}$; $T$; $x$; $v$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $T$:Type\{i\}, $x$:Id, $L$:(Knd List). $P_{1}$(Rframe(${\it loc}$; $T$; $x$; $L$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it lnk}$:IdLnk, ${\it tag}$:Id, $L$:(Knd List). $P_{1}$(Rsframe(${\it lnk}$; ${\it tag}$; $L$)))
\\[0ex]$\Rightarrow$ (\=$\forall$${\it loc}$:Id, ${\it ds}$:fpf(Id; $x$.Type\{i\}), ${\it knd}$:Knd, $T$:Type\{i\}, $x$:Id,\+
\\[0ex]$f$:(\=(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+\+
\\[0ex](${\it ds}$; $x$)) + (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$
\-\\[0ex]decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$))). $P_{1}$(Reffect(${\it loc}$; ${\it ds}$; ${\it knd}$; $T$; $x$; $f$)))
\-\-\-\\[0ex]$\Rightarrow$ \=(\=$\forall$${\it ds}$:fpf(Id; $x$.Type\{i\}), ${\it knd}$:Knd, $T$:Type\{i\}, $l$:IdLnk, ${\it dt}$:fpf(Id; $x$.Type\{i\}),\+\+
\\[0ex]$g$:((${\it tg}$:Id $\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\{i:l\}(${\it dt}$; ${\it tg}$) List))) List).
\-\\[0ex]$P_{1}$(Rsends(${\it ds}$; ${\it knd}$; $T$; $l$; ${\it dt}$; $g$)))
\-\\[0ex]$\Rightarrow$ \=($\forall$${\it loc}$:Id, ${\it ds}$:fpf(Id; $x$.Type\{i\}), $a$:Id, $p$:finite{-}prob{-}space, $P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$).\+
\\[0ex]$P_{1}$(Rpre(${\it loc}$; ${\it ds}$; $a$; $p$; $P$)))
\-\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $k$:Knd, $L$:(Id List). $P_{1}$(Raframe(${\it loc}$; $k$; $L$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $k$:Knd, $L$:(IdLnk List). $P_{1}$(Rbframe(${\it loc}$; $k$; $L$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$,$x$:Id, $L$:(Knd List). $P_{1}$(Rrframe(${\it loc}$; $x$; $L$)))
\\[0ex]$\Rightarrow$ guard(($\forall$$x_{1}$:es\_realizer\{i:l\}. $P_{1}$($x_{1}$)))
\end{tabbing}